$\forall$$A$:Type\{i\}, $P$:($A$$\rightarrow\mathbb{P}$\{i\}), $B$:($A$$\rightarrow$Type\{i'\}). $a$:\{$a$:$A$$\mid$ $P$($a$)\}  fp$\rightarrow$ $B$($a$) $\subseteq$r $a$:$A$ fp$\rightarrow$ $B$($a$)